This paper develops the very basic notions of analysis in a weak second-order theory of arithmetic BTFA whose provably total functions are the polynomial time computable functions. We formalize within BTFA the real number system and the notion of a continuous real function of a real variable. The theory BTFA is able to prove the intermediate value theorem, wherefore it follows that the system of real numbers is a real closed ordered field. In the last section of the paper, we (...) show how to interpret the theory BTFA in Robinson's theory of arithmetic Q. This fact entails that the elementary theory of the real closed ordered fields is interpretable in Q. (shrink)

We prove two conservation results involving a generalization of the principle of strict ${\Pi^1_1}$ -reflection, in the context of bounded arithmetic. In this context a separation between the concepts of bounded set and binary sequence seems to emerge as fundamental.

In this paper we give a partial answer to a conjecture of Tanaka. We prove that: if WKL0 proves a sentence of the form (∀X)(∃!Y)ψ(X, Y) for a Σ03-formula ψ, then so does RCA0.

Vertebrates respond to light with more than just their eyes. In this article, we speculate on the intriguing possibility that a link remains between non‐visual opsins and neurohormonal systems that control neuronal circuit formation and activity in mammals. Historically, the retina and pineal gland were considered the only significant light‐sensing tissues in vertebrates. However over the last century, evidence has accumulated arguing that extra‐ocular tissues in vertebrates influence behavior through non‐image‐forming photoreception. One such class of extra‐ocular light detectors are the (...) long mysterious deep brain photoreceptors. Here, we review recent findings on the cellular identity and the function of deep brain photoreceptors controlling behavior and physiology in zebrafish, and discuss their implications. (shrink)

Vertebrates respond to light with more than just their eyes. In this article, we speculate on the intriguing possibility that a link remains between non‐visual opsins and neurohormonal systems that control neuronal circuit formation and activity in mammals. Historically, the retina and pineal gland were considered the only significant light‐sensing tissues in vertebrates. However over the last century, evidence has accumulated arguing that extra‐ocular tissues in vertebrates influence behavior through non‐image‐forming photoreception. One such class of extra‐ocular light detectors are the (...) long mysterious deep brain photoreceptors. Here, we review recent findings on the cellular identity and the function of deep brain photoreceptors controlling behavior and physiology in zebrafish, and discuss their implications. (shrink)